Beginning of Section Topology
Definition. We define
open_in to be
λX T U ⇒ topology_on X T ∧ U ∈ T of type
set → set → set → prop .
Proof: Let X, T and U be given.
Apply andI to the current goal.
An exact proof term for the current goal is Htop .
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU .
∎
Definition. We define
finer_than to be
λT' T ⇒ T ⊆ T' of type
set → set → prop .
Definition. We define
coarser_than to be
λT' T ⇒ T' ⊆ T of type
set → set → prop .
Proof: Let X be given.
Assume Hfin .
Apply Hfin to the current goal.
Let n be given.
We prove the intermediate
claim Hn :
n ∈ ω .
An
exact proof term for the current goal is
(andEL (n ∈ ω ) (equip X n ) Hpair ) .
We prove the intermediate
claim Heq :
equip X n .
An
exact proof term for the current goal is
(andER (n ∈ ω ) (equip X n ) Hpair ) .
We prove the intermediate
claim Hn_sub :
n ⊆ ω .
We prove the intermediate
claim Hcount_n :
atleastp n ω .
An
exact proof term for the current goal is
(Subq_atleastp n ω Hn_sub ) .
We prove the intermediate
claim Hcount_X :
atleastp X n .
An
exact proof term for the current goal is
(atleastp_tra X n ω Hcount_X Hcount_n ) .
∎
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An
exact proof term for the current goal is
(Subq_ref (𝒫 X ) ) .
Apply PowerI to the current goal.
An
exact proof term for the current goal is
(Subq_ref X ) .
We will
prove ∀UFam ∈ 𝒫 (𝒫 X ) , ⋃ UFam ∈ 𝒫 X .
Let UFam be given.
Apply PowerI X (⋃ UFam ) to the current goal.
Let x be given.
Let U be given.
We prove the intermediate
claim HFamSub :
UFam ⊆ 𝒫 X .
An
exact proof term for the current goal is
(iffEL (UFam ∈ 𝒫 (𝒫 X ) ) (UFam ⊆ 𝒫 X ) (PowerEq (𝒫 X ) UFam ) Hfam ) .
We prove the intermediate
claim HUinPower :
U ∈ 𝒫 X .
An exact proof term for the current goal is HFamSub U HUinFam .
We prove the intermediate
claim HUsub :
U ⊆ X .
An
exact proof term for the current goal is
(iffEL (U ∈ 𝒫 X ) (U ⊆ X ) (PowerEq X U ) HUinPower ) .
An exact proof term for the current goal is (HUsub x HUinx ) .
We will
prove ∀U ∈ 𝒫 X , ∀V ∈ 𝒫 X , U ∩ V ∈ 𝒫 X .
Let U be given.
Let V be given.
Apply PowerI X (U ∩ V ) to the current goal.
Let x be given.
Assume HxU HxV .
We prove the intermediate
claim HUsub :
U ⊆ X .
An
exact proof term for the current goal is
(iffEL (U ∈ 𝒫 X ) (U ⊆ X ) (PowerEq X U ) HU ) .
An exact proof term for the current goal is (HUsub x HxU ) .
∎
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
rewrite the current goal using HUe (from left to right).
rewrite the current goal using HUX (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
Let UFam be given.
Apply xm (∃U : set , U ∈ UFam ∧ U = X ) to the current goal.
We prove the intermediate
claim HUnion_sub :
⋃ UFam ⊆ X .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (Hsub U HUin ) .
We prove the intermediate
claim HxEmpty :
x ∈ Empty .
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU .
An
exact proof term for the current goal is
(EmptyE x HxEmpty (x ∈ X ) ) .
rewrite the current goal using HUX (from right to left).
An exact proof term for the current goal is HxU .
We prove the intermediate
claim HX_sub :
X ⊆ ⋃ UFam .
Let x be given.
Assume HxX .
Apply Hex to the current goal.
Let U be given.
We prove the intermediate
claim HUin :
U ∈ UFam .
An
exact proof term for the current goal is
(andEL (U ∈ UFam ) (U = X ) HUinpair ) .
We prove the intermediate
claim HUeq :
U = X .
An
exact proof term for the current goal is
(andER (U ∈ UFam ) (U = X ) HUinpair ) .
We prove the intermediate
claim HxU :
x ∈ U .
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HxX .
Apply UnionI UFam x U HxU HUin to the current goal.
We prove the intermediate
claim HUnion_eq :
⋃ UFam = X .
An exact proof term for the current goal is HUnion_sub .
An exact proof term for the current goal is HX_sub .
rewrite the current goal using HUnion_eq (from left to right).
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
We prove the intermediate
claim HUnion_empty :
⋃ UFam = Empty .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (Hsub U HUin ) .
We prove the intermediate
claim HxEmpty :
x ∈ Empty .
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU .
An exact proof term for the current goal is HxEmpty .
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUin .
An exact proof term for the current goal is HUX .
rewrite the current goal using HUnion_empty (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
Let U be given.
Let V be given.
We prove the intermediate
claim Hcap :
U ∩ V = Empty .
rewrite the current goal using HUe (from left to right).
rewrite the current goal using Hcap (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
We prove the intermediate
claim Hcap :
U ∩ V = Empty .
rewrite the current goal using HVe (from left to right).
rewrite the current goal using Hcap (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
We prove the intermediate
claim Hcap :
U ∩ V = X .
rewrite the current goal using HUX (from left to right).
rewrite the current goal using HVX (from left to right).
Let x be given.
Assume HxX .
rewrite the current goal using HUX (from left to right).
rewrite the current goal using HVX (from left to right).
An
exact proof term for the current goal is
(binintersectI X X x HxX HxX ) .
rewrite the current goal using Hcap (from left to right).
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
∎
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
We prove the intermediate
claim Hdiff_empty :
X ∖ X = Empty .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X X x Hx ) .
We prove the intermediate
claim Hxnot :
x ∉ X .
An
exact proof term for the current goal is
(setminusE2 X X x Hx ) .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot HxX ) .
We prove the intermediate
claim HfinDiff :
finite (X ∖ X ) .
rewrite the current goal using Hdiff_empty (from left to right).
Let UFam be given.
Apply xm (∃U : set , U ∈ UFam ∧ finite (X ∖ U ) ) to the current goal.
We prove the intermediate
claim HUnionInPower :
⋃ UFam ∈ 𝒫 X .
Apply PowerI X (⋃ UFam ) to the current goal.
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
We prove the intermediate
claim HUinPow :
U ∈ 𝒫 X .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U (Hsub U HUin ) ) .
We prove the intermediate
claim HUsub :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U HUinPow ) .
An exact proof term for the current goal is (HUsub x HxU ) .
We prove the intermediate
claim HUnionPred :
finite (X ∖ ⋃ UFam ) ∨ ⋃ UFam = Empty .
Apply orIL to the current goal.
Apply Hex to the current goal.
Let U be given.
We prove the intermediate
claim HUin :
U ∈ UFam .
An
exact proof term for the current goal is
(andEL (U ∈ UFam ) (finite (X ∖ U ) ) Hpair ) .
We prove the intermediate
claim HUfin :
finite (X ∖ U ) .
An
exact proof term for the current goal is
(andER (U ∈ UFam ) (finite (X ∖ U ) ) Hpair ) .
We prove the intermediate
claim Hsubset :
X ∖ ⋃ UFam ⊆ X ∖ U .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X (⋃ UFam ) x Hx ) .
We prove the intermediate
claim HnotUnion :
x ∉ ⋃ UFam .
An
exact proof term for the current goal is
(setminusE2 X (⋃ UFam ) x Hx ) .
We prove the intermediate
claim HnotU :
x ∉ U .
Assume HxU .
Apply HnotUnion to the current goal.
Apply UnionI UFam x U HxU HUin to the current goal.
Apply setminusI X U x HxX HnotU to the current goal.
An
exact proof term for the current goal is
(Subq_finite (X ∖ U ) HUfin (X ∖ ⋃ UFam ) Hsubset ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) (⋃ UFam ) HUnionInPower HUnionPred ) .
We prove the intermediate
claim HUnionEmpty :
⋃ UFam = Empty .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U (Hsub U HUin ) ) .
Apply HUdata (x ∈ Empty ) to the current goal.
Assume HUfin .
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUin .
An exact proof term for the current goal is HUfin .
rewrite the current goal using HUempty (from right to left).
An exact proof term for the current goal is HxU .
rewrite the current goal using HUnionEmpty (from left to right).
An exact proof term for the current goal is HEmptyOpen .
Let U be given.
Let V be given.
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) V HV ) .
Assume HUfin .
Assume HVfin .
We prove the intermediate
claim HcapInPower :
U ∩ V ∈ 𝒫 X .
We prove the intermediate
claim HUsub :
U ⊆ X .
Apply PowerI X (U ∩ V ) to the current goal.
Let x be given.
Assume HxCap .
Assume HxU HxV .
An exact proof term for the current goal is (HUsub x HxU ) .
Apply orIL to the current goal.
We prove the intermediate
claim HfinUnion :
finite ((X ∖ U ) ∪ (X ∖ V ) ) .
An
exact proof term for the current goal is
(binunion_finite (X ∖ U ) HUfin (X ∖ V ) HVfin ) .
We prove the intermediate
claim Hsubset :
X ∖ (U ∩ V ) ⊆ (X ∖ U ) ∪ (X ∖ V ) .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X (U ∩ V ) x Hx ) .
We prove the intermediate
claim HnotCap :
x ∉ U ∩ V .
An
exact proof term for the current goal is
(setminusE2 X (U ∩ V ) x Hx ) .
Apply xm (x ∈ U ) to the current goal.
Assume HxU .
We prove the intermediate
claim HnotV :
x ∉ V .
Assume HxV .
Apply HnotCap to the current goal.
An
exact proof term for the current goal is
(binintersectI U V x HxU HxV ) .
Apply setminusI X V x HxX HnotV to the current goal.
Assume HnotU .
Apply setminusI X U x HxX HnotU to the current goal.
An
exact proof term for the current goal is
(Subq_finite ((X ∖ U ) ∪ (X ∖ V ) ) HfinUnion (X ∖ (U ∩ V ) ) Hsubset ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) (U ∩ V ) HcapInPower HcapPred ) .
We prove the intermediate
claim Hcap_empty :
U ∩ V = Empty .
rewrite the current goal using HVempty (from left to right).
rewrite the current goal using Hcap_empty (from left to right).
An exact proof term for the current goal is HEmptyOpen .
We prove the intermediate
claim Hcap_empty :
U ∩ V = Empty .
rewrite the current goal using HUempty (from left to right).
rewrite the current goal using Hcap_empty (from left to right).
An exact proof term for the current goal is HEmptyOpen .
∎
Proof: Let T be given.
An
exact proof term for the current goal is
(Subq_ref T ) .
∎
Proof: Let A, B and C be given.
An
exact proof term for the current goal is
(Subq_tra A B C H1 H2 ) .
∎
Proof: Let T and T' be given.
Assume H .
An exact proof term for the current goal is H .
∎
Proof: Let X, T1 and T2 be given.
Assume H .
We prove the intermediate
claim Heq :
T1 = T2 .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT2 .
An exact proof term for the current goal is HT1 .
rewrite the current goal using Heq (from right to left).
Use reflexivity.
∎
Proof: Let X, T1, T2 and T3 be given.
Assume H12 H23 .
We prove the intermediate
claim H12eq :
T1 = T2 .
We prove the intermediate
claim H23eq :
T2 = T3 .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT1 .
An exact proof term for the current goal is HT3 .
rewrite the current goal using H12eq (from left to right).
rewrite the current goal using H23eq (from left to right).
Use reflexivity.
∎
Proof: Let X and T be given.
Assume HT .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT .
An exact proof term for the current goal is HT .
∎
Proof: Let T and T' be given.
Apply iffI to the current goal.
Assume H .
An exact proof term for the current goal is H .
Assume H .
An exact proof term for the current goal is H .
∎
Proof: Let X and T be given.
Assume HT .
We prove the intermediate
claim H1 :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) HT ) .
We prove the intermediate
claim H2 :
(T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T .
An
exact proof term for the current goal is
(andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) H1 ) .
We prove the intermediate
claim H3 :
T ⊆ 𝒫 X ∧ Empty ∈ T .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) H2 ) .
We prove the intermediate
claim HTsub :
T ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ) (Empty ∈ T ) H3 ) .
An exact proof term for the current goal is HTsub .
∎
Proof: Let X and T be given.
Assume HT .
We prove the intermediate
claim Hchunk1 :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) HT ) .
We prove the intermediate
claim Hchunk2 :
(T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T .
An
exact proof term for the current goal is
(andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) Hchunk1 ) .
We prove the intermediate
claim Hchunk3 :
T ⊆ 𝒫 X ∧ Empty ∈ T .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) Hchunk2 ) .
We prove the intermediate
claim Hempty :
Empty ∈ T .
An
exact proof term for the current goal is
(andER (T ⊆ 𝒫 X ) (Empty ∈ T ) Hchunk3 ) .
We prove the intermediate
claim HX :
X ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ) ∧ Empty ∈ T ) (X ∈ T ) Hchunk2 ) .
Let U be given.
rewrite the current goal using HUempty (from left to right).
An exact proof term for the current goal is Hempty .
rewrite the current goal using HUX (from left to right).
An exact proof term for the current goal is HX .
∎
Proof: Let X and U be given.
Assume HUsub .
Apply PowerI X U HUsub to the current goal.
∎
Proof: Let X and U be given.
Apply iffI to the current goal.
Assume HU .
An
exact proof term for the current goal is
(UPairE U Empty X HU ) .
rewrite the current goal using HUE (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
rewrite the current goal using HUX (from left to right).
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
An
exact proof term for the current goal is
(Hcases (U ∈ indiscrete_topology X ) HUempty_branch HUx_branch ) .
∎
Proof: Let X and U be given.
Assume Hopen .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HUin ) .
∎
Proof: Let X be given.
We prove the intermediate
claim Hdiff_empty :
X ∖ X = Empty .
Let x be given.
Assume Hx .
We prove the intermediate
claim Hxin :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X X x Hx ) .
We prove the intermediate
claim Hxnot :
x ∉ X .
An
exact proof term for the current goal is
(setminusE2 X X x Hx ) .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot Hxin ) .
We prove the intermediate
claim HfinDiff :
finite (X ∖ X ) .
rewrite the current goal using Hdiff_empty (from left to right).
∎
Proof: Let X and U be given.
Assume Hopen .
∎
Proof: Let X be given.
We prove the intermediate
claim Hdiff_empty :
X ∖ X = Empty .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X X x Hx ) .
We prove the intermediate
claim Hxnot :
x ∉ X .
An
exact proof term for the current goal is
(setminusE2 X X x Hx ) .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot HxX ) .
We prove the intermediate
claim HcountDiff :
countable (X ∖ X ) .
rewrite the current goal using Hdiff_empty (from left to right).
∎
Proof: Let X be given.
Let U be given.
We prove the intermediate
claim HUinPow :
U ∈ 𝒫 X .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is HUemp .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ countable (X ∖ U0 ) ∨ U0 = Empty ) U HUinPow HUpred ) .
∎
Proof: Let X be given.
Let U be given.
Assume HU .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
∎
Proof: Let X be given.
Let U be given.
rewrite the current goal using HUempty (from left to right).
rewrite the current goal using HUX (from left to right).
∎
Proof: Let X, T' and T be given.
Apply iffI to the current goal.
Assume H .
An exact proof term for the current goal is H .
Assume H .
An exact proof term for the current goal is H .
∎
Proof: Let X, T and UFam be given.
Assume HT Hfam .
We prove the intermediate
claim Hchunk1 :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) HT ) .
We prove the intermediate
claim Hunion_axiom :
∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T ) Hchunk1 ) .
An exact proof term for the current goal is (Hunion_axiom UFam Hfam ) .
∎
Proof: Let X, T, U and V be given.
Assume HT HU HV .
We prove the intermediate
claim Hax_inter :
∀U' ∈ T , ∀V' ∈ T , U' ∩ V' ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T ∧ X ∈ T ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) ) (∀U' ∈ T , ∀V' ∈ T , U' ∩ V' ∈ T ) HT ) .
An exact proof term for the current goal is (Hax_inter U HU V HV ) .
∎
Definition. We define
open_set_family to be
λ_ T ⇒ T of type
set → set → set .
Definition. We define
basis_on to be
λX B ⇒ B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ∧ (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) of type
set → set → prop .
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBleft :
B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) .
We prove the intermediate
claim HBint :
∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) HBleft ) .
We prove the intermediate
claim HBcov :
∀x ∈ X , ∃b ∈ B , x ∈ b .
An
exact proof term for the current goal is
(andER (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) HBleft ) .
Let U be given.
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) U HU ) .
We prove the intermediate
claim HXprop :
∀x ∈ X , ∃b ∈ B , x ∈ b ∧ b ⊆ X .
Let x be given.
Assume HxX .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b .
An exact proof term for the current goal is (HBcov x HxX ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ) Hbpair ) .
We prove the intermediate
claim HbsubX :
b ⊆ X .
An
exact proof term for the current goal is
(PowerE X b (HBsub b HbB ) ) .
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb .
An exact proof term for the current goal is HbsubX .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) X (Self_In_Power X ) HXprop ) .
Let UFam be given.
We prove the intermediate
claim HPowUnion :
⋃ UFam ∈ 𝒫 X .
Apply PowerI X (⋃ UFam ) to the current goal.
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (HsubFam U HUin ) .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) ) .
An exact proof term for the current goal is (HUsubX x HxU ) .
We prove the intermediate
claim HUnionProp :
∀x ∈ ⋃ UFam , ∃b ∈ B , x ∈ b ∧ b ⊆ ⋃ UFam .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (HsubFam U HUin ) .
We prove the intermediate
claim HUprop :
∀x0 ∈ U , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbSubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb .
Let y be given.
Assume Hyb .
Apply UnionI UFam y U (HbSubU y Hyb ) HUin to the current goal.
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) (⋃ UFam ) HPowUnion HUnionProp ) .
Let U be given.
Assume HUtop .
Let V be given.
Assume HVtop .
We prove the intermediate
claim HUprop :
∀x0 ∈ U , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
We prove the intermediate
claim HVprop :
∀x0 ∈ V , ∃b ∈ B , x0 ∈ b ∧ b ⊆ V .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) V HVtop ) .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) ) .
We prove the intermediate
claim HPowCap :
U ∩ V ∈ 𝒫 X .
Apply PowerI X (U ∩ V ) to the current goal.
Let x be given.
Assume HxCap .
Assume HxU HxV .
An exact proof term for the current goal is (HUsubX x HxU ) .
We prove the intermediate
claim HCapProp :
∀x ∈ U ∩ V , ∃b ∈ B , x ∈ b ∧ b ⊆ U ∩ V .
Let x be given.
Assume HxCap .
Assume HxU HxV .
We prove the intermediate
claim Hexb1 :
∃b1 ∈ B , x ∈ b1 ∧ b1 ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
We prove the intermediate
claim Hexb2 :
∃b2 ∈ B , x ∈ b2 ∧ b2 ⊆ V .
An exact proof term for the current goal is (HVprop x HxV ) .
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hbpair1 .
We prove the intermediate
claim Hb1 :
b1 ∈ B .
An
exact proof term for the current goal is
(andEL (b1 ∈ B ) (x ∈ b1 ∧ b1 ⊆ U ) Hbpair1 ) .
We prove the intermediate
claim Hb1prop :
x ∈ b1 ∧ b1 ⊆ U .
An
exact proof term for the current goal is
(andER (b1 ∈ B ) (x ∈ b1 ∧ b1 ⊆ U ) Hbpair1 ) .
We prove the intermediate
claim Hb1x :
x ∈ b1 .
An
exact proof term for the current goal is
(andEL (x ∈ b1 ) (b1 ⊆ U ) Hb1prop ) .
We prove the intermediate
claim Hb1Sub :
b1 ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b1 ) (b1 ⊆ U ) Hb1prop ) .
Apply Hexb2 to the current goal.
Let b2 be given.
Assume Hbpair2 .
We prove the intermediate
claim Hb2 :
b2 ∈ B .
An
exact proof term for the current goal is
(andEL (b2 ∈ B ) (x ∈ b2 ∧ b2 ⊆ V ) Hbpair2 ) .
We prove the intermediate
claim Hb2prop :
x ∈ b2 ∧ b2 ⊆ V .
An
exact proof term for the current goal is
(andER (b2 ∈ B ) (x ∈ b2 ∧ b2 ⊆ V ) Hbpair2 ) .
We prove the intermediate
claim Hb2x :
x ∈ b2 .
An
exact proof term for the current goal is
(andEL (x ∈ b2 ) (b2 ⊆ V ) Hb2prop ) .
We prove the intermediate
claim Hb2Sub :
b2 ⊆ V .
An
exact proof term for the current goal is
(andER (x ∈ b2 ) (b2 ⊆ V ) Hb2prop ) .
We prove the intermediate
claim Hexb3 :
∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An exact proof term for the current goal is (HBint b1 Hb1 b2 Hb2 x Hb1x Hb2x ) .
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hbpair3 .
We prove the intermediate
claim Hb3 :
b3 ∈ B .
An
exact proof term for the current goal is
(andEL (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) Hbpair3 ) .
We prove the intermediate
claim Hb3prop :
x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) Hbpair3 ) .
We prove the intermediate
claim HxB3 :
x ∈ b3 .
An
exact proof term for the current goal is
(andEL (x ∈ b3 ) (b3 ⊆ b1 ∩ b2 ) Hb3prop ) .
We prove the intermediate
claim Hb3Sub :
b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (x ∈ b3 ) (b3 ⊆ b1 ∩ b2 ) Hb3prop ) .
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3 .
Apply andI to the current goal.
An exact proof term for the current goal is HxB3 .
Let y be given.
Assume Hyb3 .
We prove the intermediate
claim Hy_in_b1b2 :
y ∈ b1 ∩ b2 .
An exact proof term for the current goal is (Hb3Sub y Hyb3 ) .
Assume Hyb1 Hyb2 .
Apply binintersectI U V y (Hb1Sub y Hyb1 ) (Hb2Sub y Hyb2 ) to the current goal.
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) (U ∩ V ) HPowCap HCapProp ) .
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is proofA .
An exact proof term for the current goal is proofB .
An exact proof term for the current goal is proofC .
An exact proof term for the current goal is proofD .
An exact proof term for the current goal is proofE .
∎
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) ) .
We prove the intermediate
claim HBint :
∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) .
Let b0 be given.
Assume Hb0 .
We prove the intermediate
claim Hb0_subX :
b0 ⊆ X .
An
exact proof term for the current goal is
(PowerE X b0 (HBsub b0 Hb0 ) ) .
We prove the intermediate
claim Hb0prop :
∀x ∈ b0 , ∃b ∈ B , x ∈ b ∧ b ⊆ b0 .
Let x be given.
Assume Hxb0 .
We prove the intermediate
claim Hexb3 :
∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 .
An exact proof term for the current goal is (HBint b0 Hb0 b0 Hb0 x Hxb0 Hxb0 ) .
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hb3pair .
We prove the intermediate
claim Hb3 :
b3 ∈ B .
An
exact proof term for the current goal is
(andEL (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 ) Hb3pair ) .
We prove the intermediate
claim Hb3prop :
x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 .
An
exact proof term for the current goal is
(andER (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 ) Hb3pair ) .
We prove the intermediate
claim Hxb3 :
x ∈ b3 .
An
exact proof term for the current goal is
(andEL (x ∈ b3 ) (b3 ⊆ b0 ∩ b0 ) Hb3prop ) .
We prove the intermediate
claim Hb3sub_inter :
b3 ⊆ b0 ∩ b0 .
An
exact proof term for the current goal is
(andER (x ∈ b3 ) (b3 ⊆ b0 ∩ b0 ) Hb3prop ) .
We prove the intermediate
claim Hb3subb0 :
b3 ⊆ b0 .
Let y be given.
Assume Hyb3 .
We prove the intermediate
claim Hycap :
y ∈ b0 ∩ b0 .
An exact proof term for the current goal is (Hb3sub_inter y Hyb3 ) .
Assume Hy1 Hy2 .
An exact proof term for the current goal is Hy1 .
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3 .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb3 .
An exact proof term for the current goal is Hb3subb0 .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) b0 (PowerI X b0 Hb0_subX ) Hb0prop ) .
∎
Proof: Let X and B be given.
Assume HBasis .
Use reflexivity.
∎
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) ) .
Let U be given.
Assume HUopen .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
Set Fam to be the term
{ b ∈ B | b ⊆ U } of type
set .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
Apply PowerI B Fam to the current goal.
Let b be given.
Assume HbFam .
An
exact proof term for the current goal is
(SepE1 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
We prove the intermediate
claim HUnion_eq :
⋃ Fam = U .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(SepE2 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HbsubU x Hxb ) .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbFam :
b ∈ Fam .
An
exact proof term for the current goal is
(SepI B (λb0 : set ⇒ b0 ⊆ U ) b HbB HbsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x b Hxb HbFam ) .
We use Fam to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamPow .
An exact proof term for the current goal is HUnion_eq .
∎
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) ) .
Let U be given.
Assume Hex .
Apply Hex to the current goal.
Let Fam be given.
Assume HFampair .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HUnionEq :
⋃ Fam = U .
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HFamSubB :
Fam ⊆ B .
An
exact proof term for the current goal is
(PowerE B Fam HFamPow ) .
We prove the intermediate
claim HFamSubX :
Fam ⊆ 𝒫 X .
Let b be given.
Assume HbFam .
We prove the intermediate
claim HbB :
b ∈ B .
An exact proof term for the current goal is (HFamSubB b HbFam ) .
An exact proof term for the current goal is (HBsub b HbB ) .
We prove the intermediate
claim HUnionSubX :
⋃ Fam ⊆ X .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbSubX :
b ⊆ X .
An
exact proof term for the current goal is
(PowerE X b (HFamSubX b HbFam ) ) .
An exact proof term for the current goal is (HbSubX x Hxb ) .
We prove the intermediate
claim HUnionSubU :
⋃ Fam ⊆ U .
rewrite the current goal using HUnionEq (from left to right).
An
exact proof term for the current goal is
(Subq_ref U ) .
We prove the intermediate
claim HUsubUnion :
U ⊆ ⋃ Fam .
rewrite the current goal using HUnionEq (from right to left).
An
exact proof term for the current goal is
(Subq_ref (⋃ Fam ) ) .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(Subq_tra U (⋃ Fam ) X HUsubUnion HUnionSubX ) .
We prove the intermediate
claim HUpropU :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
Let x be given.
Assume HxU .
We prove the intermediate
claim HxUnion :
x ∈ ⋃ Fam .
An exact proof term for the current goal is (HUsubUnion x HxU ) .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbB :
b ∈ B .
An exact proof term for the current goal is (HFamSubB b HbFam ) .
We prove the intermediate
claim HbSubUnion :
b ⊆ ⋃ Fam .
Let y be given.
Assume Hyb .
An
exact proof term for the current goal is
(UnionI Fam y b Hyb HbFam ) .
We prove the intermediate
claim HbSubU :
b ⊆ U .
An
exact proof term for the current goal is
(Subq_tra b (⋃ Fam ) U HbSubUnion HUnionSubU ) .
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb .
An exact proof term for the current goal is HbSubU .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUpropU ) .
∎
Proof: Let X and B be given.
Assume HBasis .
Let U be given.
Assume HUopen .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
Set Fam to be the term
{ b ∈ B | b ⊆ U } of type
set .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbFam :
b ∈ Fam .
An
exact proof term for the current goal is
(SepI B (λb0 : set ⇒ b0 ⊆ U ) b HbB HbsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x b Hxb HbFam ) .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(SepE2 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HbsubU x Hxb ) .
∎
Proof: Let X, T and C be given.
Assume Htop HCsub Href .
We prove the intermediate
claim Hleft :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) Htop ) .
We prove the intermediate
claim Hcore :
(T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T .
An
exact proof term for the current goal is
(andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) Hleft ) .
We prove the intermediate
claim HTPowEmpty :
T ⊆ 𝒫 X ∧ Empty ∈ T .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) Hcore ) .
We prove the intermediate
claim HTsubPow :
T ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ) (Empty ∈ T ) HTPowEmpty ) .
We prove the intermediate
claim HXT :
X ∈ T .
An
exact proof term for the current goal is
(andER (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) Hcore ) .
We prove the intermediate
claim HUnionClosed :
∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) Hleft ) .
We prove the intermediate
claim HInterClosed :
∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T .
An
exact proof term for the current goal is
(andER (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) Htop ) .
We prove the intermediate
claim HBasis :
basis_on X C .
We will
prove (C ⊆ 𝒫 X ∧ (∀x ∈ X , ∃c ∈ C , x ∈ c ) ∧ (∀b1 ∈ C , ∀b2 ∈ C , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ C , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) ) .
Apply andI to the current goal.
Apply andI to the current goal.
Let c be given.
Assume HcC .
An exact proof term for the current goal is (HTsubPow c (HCsub c HcC ) ) .
Let x be given.
Assume HxX .
We prove the intermediate
claim Hex :
∃c ∈ C , x ∈ c ∧ c ⊆ X .
An exact proof term for the current goal is (Href X HXT x HxX ) .
Apply Hex to the current goal.
Let c be given.
Assume Hpair .
We prove the intermediate
claim HcC :
c ∈ C .
An
exact proof term for the current goal is
(andEL (c ∈ C ) (x ∈ c ∧ c ⊆ X ) Hpair ) .
We prove the intermediate
claim Hcprop :
x ∈ c ∧ c ⊆ X .
An
exact proof term for the current goal is
(andER (c ∈ C ) (x ∈ c ∧ c ⊆ X ) Hpair ) .
We prove the intermediate
claim Hxc :
x ∈ c .
An
exact proof term for the current goal is
(andEL (x ∈ c ) (c ⊆ X ) Hcprop ) .
We use c to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HcC .
An exact proof term for the current goal is Hxc .
Let c1 be given.
Assume Hc1C .
Let c2 be given.
Assume Hc2C .
Let x be given.
Assume Hxc1 Hxc2 .
We prove the intermediate
claim Hc1T :
c1 ∈ T .
An exact proof term for the current goal is (HCsub c1 Hc1C ) .
We prove the intermediate
claim Hc2T :
c2 ∈ T .
An exact proof term for the current goal is (HCsub c2 Hc2C ) .
We prove the intermediate
claim HcapT :
c1 ∩ c2 ∈ T .
An exact proof term for the current goal is (HInterClosed c1 Hc1T c2 Hc2T ) .
We prove the intermediate
claim HxCap :
x ∈ c1 ∩ c2 .
An
exact proof term for the current goal is
(binintersectI c1 c2 x Hxc1 Hxc2 ) .
We prove the intermediate
claim Hex :
∃c3 ∈ C , x ∈ c3 ∧ c3 ⊆ c1 ∩ c2 .
An
exact proof term for the current goal is
(Href (c1 ∩ c2 ) HcapT x HxCap ) .
An exact proof term for the current goal is Hex .
Let U be given.
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ C , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HUgen ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃c ∈ C , x ∈ c ∧ c ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ C , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HUgen ) .
Set Fam to be the term
{ c ∈ C | c ⊆ U } of type
set .
We prove the intermediate
claim HFamSubC :
Fam ⊆ C .
Let c be given.
Assume HcFam .
An
exact proof term for the current goal is
(SepE1 C (λc0 : set ⇒ c0 ⊆ U ) c HcFam ) .
We prove the intermediate
claim HFamSubT :
Fam ⊆ T .
Let c be given.
Assume HcFam .
We prove the intermediate
claim HcC :
c ∈ C .
An exact proof term for the current goal is (HFamSubC c HcFam ) .
An exact proof term for the current goal is (HCsub c HcC ) .
We prove the intermediate
claim HFamPowT :
Fam ∈ 𝒫 T .
An
exact proof term for the current goal is
(PowerI T Fam HFamSubT ) .
We prove the intermediate
claim HUnionSubU :
⋃ Fam ⊆ U .
Let x be given.
Assume HxUnion .
Let c be given.
Assume Hxc HcFam .
We prove the intermediate
claim Hcprop :
c ⊆ U .
An
exact proof term for the current goal is
(SepE2 C (λc0 : set ⇒ c0 ⊆ U ) c HcFam ) .
An exact proof term for the current goal is (Hcprop x Hxc ) .
We prove the intermediate
claim HUsubUnion :
U ⊆ ⋃ Fam .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hex :
∃c ∈ C , x ∈ c ∧ c ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hex to the current goal.
Let c be given.
Assume Hcpair .
We prove the intermediate
claim HcC :
c ∈ C .
An
exact proof term for the current goal is
(andEL (c ∈ C ) (x ∈ c ∧ c ⊆ U ) Hcpair ) .
We prove the intermediate
claim Hcprop :
x ∈ c ∧ c ⊆ U .
An
exact proof term for the current goal is
(andER (c ∈ C ) (x ∈ c ∧ c ⊆ U ) Hcpair ) .
We prove the intermediate
claim Hxc :
x ∈ c .
An
exact proof term for the current goal is
(andEL (x ∈ c ) (c ⊆ U ) Hcprop ) .
We prove the intermediate
claim HcsubU :
c ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ c ) (c ⊆ U ) Hcprop ) .
We prove the intermediate
claim HcFam :
c ∈ Fam .
An
exact proof term for the current goal is
(SepI C (λc0 : set ⇒ c0 ⊆ U ) c HcC HcsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x c Hxc HcFam ) .
We prove the intermediate
claim HUnionEqU :
⋃ Fam = U .
Let x be given.
Assume HxUnion .
An exact proof term for the current goal is (HUnionSubU x HxUnion ) .
Let x be given.
Assume HxU .
An exact proof term for the current goal is (HUsubUnion x HxU ) .
We prove the intermediate
claim HUnionInT :
⋃ Fam ∈ T .
An exact proof term for the current goal is (HUnionClosed Fam HFamPowT ) .
rewrite the current goal using HUnionEqU (from right to left).
An exact proof term for the current goal is HUnionInT .
Let U be given.
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (HTsubPow U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃c ∈ C , x ∈ c ∧ c ⊆ U .
Let x be given.
Assume HxU .
An exact proof term for the current goal is (Href U HU x HxU ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ C , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUprop ) .
Let U be given.
Assume HUgen .
An exact proof term for the current goal is (Hgen_sub_T U HUgen ) .
Let U be given.
Assume HU .
An exact proof term for the current goal is (HT_sub_gen U HU ) .
Apply andI to the current goal.
An exact proof term for the current goal is HBasis .
An exact proof term for the current goal is HEqual .
∎
Proof: Let X, T and C be given.
Assume Htop HCsub Href .
∎
Proof: Let X, B and B' be given.
Assume HB HB' Hcond .
Let U be given.
Let x be given.
Assume HxU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HUsubX x HxU ) .
We prove the intermediate
claim HUprop :
∀x0 ∈ U , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HU ) .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim Hexb' :
∃b' ∈ B' , x ∈ b' ∧ b' ⊆ b .
An exact proof term for the current goal is (Hcond x HxX b HbB Hxb ) .
Apply Hexb' to the current goal.
Let b' be given.
Assume Hb'pair .
We prove the intermediate
claim Hb'B :
b' ∈ B' .
An
exact proof term for the current goal is
(andEL (b' ∈ B' ) (x ∈ b' ∧ b' ⊆ b ) Hb'pair ) .
We prove the intermediate
claim Hb'prop :
x ∈ b' ∧ b' ⊆ b .
An
exact proof term for the current goal is
(andER (b' ∈ B' ) (x ∈ b' ∧ b' ⊆ b ) Hb'pair ) .
We prove the intermediate
claim Hxb' :
x ∈ b' .
An
exact proof term for the current goal is
(andEL (x ∈ b' ) (b' ⊆ b ) Hb'prop ) .
We prove the intermediate
claim Hb'subb :
b' ⊆ b .
An
exact proof term for the current goal is
(andER (x ∈ b' ) (b' ⊆ b ) Hb'prop ) .
We use b' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb'B .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb' .
An
exact proof term for the current goal is
(Subq_tra b' b U Hb'subb HbsubU ) .
Let U be given.
Assume HU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b' ∈ B' , x ∈ b' ∧ b' ⊆ U .
An exact proof term for the current goal is (HRefProp U HU ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B' , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUprop ) .
∎
Proof: Let X, B and B' be given.
Assume HB HB' .
Apply iffI to the current goal.
Assume Hcond .
An
exact proof term for the current goal is
(finer_via_basis X B B' HB HB' Hcond ) .
Assume Hfiner .
Let x be given.
Assume HxX .
Let b be given.
Assume HbB Hxb .
An exact proof term for the current goal is (Hfiner b HbGen ) .
We prove the intermediate
claim Hbprop :
∀x0 ∈ b , ∃b' ∈ B' , x0 ∈ b' ∧ b' ⊆ b .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B' , x0 ∈ b0 ∧ b0 ⊆ U0 ) b HbGen' ) .
An exact proof term for the current goal is (Hbprop x Hxb ) .
∎
Proof: Let X, B and T be given.
Assume HBasis HT HBsub .
We prove the intermediate
claim HUnionClosed :
∀Fam ∈ 𝒫 T , ⋃ Fam ∈ T .
Let U be given.
Assume HU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) .
Set Fam to be the term
{ b ∈ B | b ⊆ U } of type
set .
We prove the intermediate
claim HFamPowB :
Fam ∈ 𝒫 B .
Apply PowerI B Fam to the current goal.
Let b be given.
Assume HbFam .
An
exact proof term for the current goal is
(SepE1 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
We prove the intermediate
claim HUnionEq :
⋃ Fam = U .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(SepE2 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HbsubU x Hxb ) .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbT :
b ∈ T .
An exact proof term for the current goal is (HBsub b HbB ) .
We prove the intermediate
claim HbFam :
b ∈ Fam .
An
exact proof term for the current goal is
(SepI B (λb0 : set ⇒ b0 ⊆ U ) b HbB HbsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x b Hxb HbFam ) .
We prove the intermediate
claim HFamPowT :
Fam ∈ 𝒫 T .
Apply PowerI T Fam to the current goal.
Let b be given.
Assume HbFam .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(SepE1 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HBsub b HbB ) .
We prove the intermediate
claim HUnionT :
⋃ Fam ∈ T .
An exact proof term for the current goal is (HUnionClosed Fam HFamPowT ) .
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionT .
∎
Proof: Let X, B and T be given.
Assume HBasis HT HBsub .
∎
Proof: Let X and B be given.
Assume HBasis .
Let U be given.
Assume HU .
We prove the intermediate
claim HexFam :
∃Fam ∈ 𝒫 B , ⋃ Fam = U .
Apply HexFam to the current goal.
Let Fam be given.
Assume HFampair .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HUnion :
⋃ Fam = U .
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HUnionFam :
⋃ Fam ∈ { ⋃ Fam0 | Fam0 ∈ 𝒫 B } .
An
exact proof term for the current goal is
(ReplI (𝒫 B ) (λFam0 : set ⇒ ⋃ Fam0 ) Fam HFamPow ) .
rewrite the current goal using HUnion (from right to left).
An exact proof term for the current goal is HUnionFam .
Let U be given.
Assume HUUnion .
We prove the intermediate
claim HexFamPowRaw :
∃Fam ∈ 𝒫 B , U = ⋃ Fam .
An
exact proof term for the current goal is
(ReplE (𝒫 B ) (λFam0 : set ⇒ ⋃ Fam0 ) U HUUnion ) .
We prove the intermediate
claim HexFamPow :
∃Fam ∈ 𝒫 B , ⋃ Fam = U .
Apply HexFamPowRaw to the current goal.
Let Fam be given.
Assume HFamPair .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B ) (U = ⋃ Fam ) HFamPair ) .
We prove the intermediate
claim HUnion :
U = ⋃ Fam .
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B ) (U = ⋃ Fam ) HFamPair ) .
We use Fam to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamPow .
rewrite the current goal using HUnion (from right to left).
Use reflexivity.
∎
Proof: The rest of this subproof is missing.
∎
Proof: Let X be given.
Let U be given.
Assume HUgen .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ singleton_basis X , x0 ∈ b ∧ b ⊆ U0 ) U HUgen ) .
Let U be given.
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U HUinPow ) .
Let x be given.
Assume HxU .
We use
{ x , x } to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
(ReplI X (λx0 : set ⇒ { x0 , x0 } ) x (HUsubX x HxU ) ) .
Apply andI to the current goal.
An
exact proof term for the current goal is
(UPairI1 x x ) .
Let y be given.
Assume Hy .
Apply (UPairE y x x Hy (y ∈ U ) ) to the current goal.
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxU .
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxU .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ singleton_basis X , x0 ∈ b ∧ b ⊆ U0 ) U HUinPow HUprop ) .
∎
Definition. We define
R to be
real of type
set .
Definition. We define
Rlt to be
λa b ⇒ a ∈ R ∧ b ∈ R ∧ a < b of type
set → set → prop .
Definition. We define
distance_R2 to be
λp c ⇒ Eps_i (λr ⇒ r ∈ R ) of type
set → set → set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: Let X, B and B' be given.
Assume HBasis Href .
Let U be given.
Assume HU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b' ∈ B' , x ∈ b' ∧ b' ⊆ U .
An exact proof term for the current goal is (Hprop U HU ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B' , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUprop ) .
∎
Definition. We define
subbasis_on to be
λX S ⇒ S ⊆ 𝒫 X of type
set → set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
a_elt to be
Empty of type
set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
K_set to be
ω of type
set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
open_ray_upper to be
λX a ⇒ X of type
set → set → set .
Definition. We define
open_ray_lower to be
λX a ⇒ X of type
set → set → set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
Zplus to be
ω of type
set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
function_on to be
λf X Y ⇒ ∀x : set , x ∈ X → apply_fun f x ∈ Y of type
set → set → set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: Let W, Y and A be given.
Let x be given.
We prove the intermediate
claim Hpair :
x ∈ W ∩ Y ∧ x ∈ A .
An
exact proof term for the current goal is
(binintersectE (W ∩ Y ) A x Hx ) .
We prove the intermediate
claim HWY :
x ∈ W ∩ Y .
An
exact proof term for the current goal is
(andEL (x ∈ W ∩ Y ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HA :
x ∈ A .
An
exact proof term for the current goal is
(andER (x ∈ W ∩ Y ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HWYpair :
x ∈ W ∧ x ∈ Y .
An
exact proof term for the current goal is
(binintersectE W Y x HWY ) .
We prove the intermediate
claim HW :
x ∈ W .
An
exact proof term for the current goal is
(andEL (x ∈ W ) (x ∈ Y ) HWYpair ) .
An exact proof term for the current goal is HW .
An exact proof term for the current goal is HA .
Let x be given.
We prove the intermediate
claim Hpair :
x ∈ W ∧ x ∈ A .
An
exact proof term for the current goal is
(binintersectE W A x Hx ) .
We prove the intermediate
claim HW :
x ∈ W .
An
exact proof term for the current goal is
(andEL (x ∈ W ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HA :
x ∈ A .
An
exact proof term for the current goal is
(andER (x ∈ W ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HY :
x ∈ Y .
An exact proof term for the current goal is (Hsub x HA ) .
We prove the intermediate
claim HWY :
x ∈ W ∩ Y .
An
exact proof term for the current goal is
(binintersectI W Y x HW HY ) .
An exact proof term for the current goal is HWY .
An exact proof term for the current goal is HA .
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
interior_of to be
λX T A ⇒ { x ∈ X | ∃U : set , U ∈ T ∧ x ∈ U ∧ U ⊆ A } of type
set → set → set → set .
Definition. We define
closure_of to be
λX T A ⇒ { x ∈ X | ∀U : set , U ∈ T → x ∈ U → U ∩ A ≠ Empty } of type
set → set → set → set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
open_ball to be
λX d x ⇒ { y ∈ X | ∃r ∈ R , Rlt (d x y ) r } of type
set → set → set → set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
sequence_in to be
λseq A ⇒ seq ⊆ A of type
set → set → prop .
Definition. We define
image_of to be
λf seq ⇒ Repl seq (λy ⇒ y ) of type
set → set → set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
covers to be
λX U ⇒ ∀x : set , x ∈ X → ∃u : set , u ∈ U ∧ x ∈ u of type
set → set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
Abs to be
abs_SNo of type
set → set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
directed_set to be
λJ ⇒ J ≠ Empty ∧ ∀i j : set , i ∈ J → j ∈ J → ∃k : set , k ∈ J of type
set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
open_cover to be
λX Tx U ⇒ (∀u : set , u ∈ U → u ∈ Tx ) ∧ covers X U of type
set → set → set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
dense_in to be
λA X Tx ⇒ closure_of X Tx A = X of type
set → set → set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
R_K to be
R of type
set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
S_Omega to be
ω of type
set .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Definition. We define
refine_of to be
λV U ⇒ ∀v : set , v ∈ V → ∃u : set , u ∈ U ∧ v ⊆ u of type
set → set → prop .
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎
Proof: The rest of this subproof is missing.
∎